18 result(s)
Page Size: 10, 20, 50
Export: bibtex, xml, json, csv
Order by:

CNR Author operator: and / or
more
Typology operator: and / or
Language operator: and / or
Date operator: and / or
Rights operator: and / or
2023 Contribution to book Open Access OPEN
A case study in formal analysis of system requirements
Belli D., Mazzanti F.
One of the goals of the 4SECURail project has been to demonstrate the benefits, limits, and costs of introducing formal meth- ods in the system requirements definition process. This has been done, on an experimental basis, by applying a specific set of tools and method- ologies to a case study from the railway sector. The paper describes the approach adopted in the project and some considerations resulting from the experience.Source: Software Engineering and Formal Methods. SEFM 2022 Collocated Workshops, edited by Masci P., Bernardeschi C., Graziani P., Koddenbrock M., Palmieri M., pp. 164–173, 2023
DOI: 10.1007/978-3-031-26236-4_14
Project(s): 4SECURAIL via OpenAIRE
Metrics:


See at: ISTI Repository Open Access | doi.org Restricted | link.springer.com Restricted | CNR ExploRA


2023 Conference article Open Access OPEN
The 4SECURail case study on rigorous standard interface specifications
Belli D., Fantechi A., Gnesi S., Masullo L., Mazzanti F., Quadrini L., Trentini D., Vaghi C.
In the context of the Shift2Rail open call S2R-OC-IP2-01- 2019, one of the two work streams of the 4SECURail project has pursued the objective to corroborate how a clear, rigorous standard interface specification between signaling sub-systems can be designed by applying an approach based on semi-formal and formal methods. The objective is addressed by developing a demonstrator case study of the application of formal methods to the specification of standard interfaces, aimed at illustrating some usable state-of-the-art techniques for rigorous standard interface specification, as well as at supporting a Cost-Benefit Analysis to back this strategy with sound economic arguments.Source: FMICS 2023 - 28th International Conference on Formal Methods for Industrial Critical Systems, pp. 22–39, Antwerp, Belgium, 20-22/09/2023
DOI: 10.1007/978-3-031-43681-9_2
Project(s): 4SECURAIL via OpenAIRE
Metrics:


See at: ISTI Repository Open Access | link.springer.com Restricted | CNR ExploRA


2023 Journal article Open Access OPEN
Connectivity standards alliance matter: state of the art and opportunities
Belli D., Barsocchi P., Palumbo F.
Matter is an open-source, royalty-free connectivity standard developed by the Connectivity Standards Alliance (CSA-IoT). It aims to unify smart home devices and increase their compatibility across various ecosystems. Backed by major tech companies like Apple, Google, Amazon, and the Zigbee Alliance, Matter simplifies the development of IoT devices by providing a unified approach to connectivity. It offers a secure, reliable, and seamless way for devices to communicate and interact, regardless of the manufacturer. This paper aims to present the current state of adoption of the Matter specification by devices available on the market, and the certification process by the available software. It describes the main characteristics of Matter in its Specification 1.0 state, reviewing the features and functionalities of the Matter protocol, as well as the opportunities for its use and the challenges for its large-scale adoption in Matter-compliant IoT devices. We discuss the impact of Matter on IoT technologies and ecosystems, providing guidance for manufacturers and consumers. We analyze the emerging research challenges in its adoption and propose our recommendations on how to improve and extend this protocol for better use in the future.Source: Internet of Things 25 (2023). doi:10.1016/j.iot.2023.101005
DOI: 10.1016/j.iot.2023.101005
Metrics:


See at: ISTI Repository Open Access | www.sciencedirect.com Open Access | CNR ExploRA


2022 Conference article Open Access OPEN
Formal modeling and initial analysis of the 4SECURail case study
Mazzanti F., Belli D.
We present the case study developed in the context of the 4SECURail project and the approach used for its formal modeling and analysis. Starting from a simple SysML/UML behavioral model of the system requirements, three formal models have been developed using three different frameworks, namely UMC, ProB, and CADP/LNT. The paper shows how the different ways to represent and analyze the system from the three different points of view allow us to take advantage of the resulting diversity.Source: MARS 2022 - Fifth Workshop on Models for Formal Analysis of Real Systems, pp. 118–144, Munich, DE, 01/04/2022
DOI: 10.4204/eptcs.355.6
Project(s): 4SECURAIL via OpenAIRE
Metrics:


See at: eptcs.web.cse.unsw.edu.au Open Access | ISTI Repository Open Access | CNR ExploRA


2022 Software Unknown
Multivariate time series dataset generator
Belli D., Miori V.
A Java class that provides constructors and methods to generate synthetic data sets of multi-variate time series with/without anomalies. The class Random is used to introduce the right percentage of aleatority to the generation of the signals. Temporal patterns have been modeled based on trigonometric functions, randomly selected feature by feature. To reproduce the anomalies, a little noise is added to the generated signals. The class has been designed to test machine learning algorithms developed for anomaly detection in multivariate time series data.

See at: github.com | CNR ExploRA


2022 Conference article Open Access OPEN
The 4SECURail formal methods demonstrator
Mazzanti F., Belli D.
The need for high-quality standard interfaces is widely recognized as a mandatory step to reduce procurement costs and create safely operating complex railway infrastructures. That is why European initiatives like EULYNX have been set up precisely with the purpose of supporting standard interfaces development. The exploitation of formal methods during the phase of standardization plays an essential role in raising the quality of the generated specifications. 4SECURail is a recent project that aims to precisely show, with a structured evaluation (known as the formal methods demonstrator), how formal methods might help to improve the quality of a specific signalling interface selected as case study. This paper describes the experience gained with the experiment.Source: RSSRail 2022 - 4th International Conference on Reliability, Safety, and Security of Railway Systems, pp. 149–165, Paris, France, 1-2/06/2022
DOI: 10.1007/978-3-031-05814-1_11
DOI: 10.5281/zenodo.6245955
DOI: 10.5281/zenodo.6245956
Project(s): 4SECURAIL via OpenAIRE
Metrics:


See at: ZENODO Open Access | ZENODO Open Access | ISTI Repository Open Access | doi.org Restricted | link.springer.com Restricted | CNR ExploRA


2022 Conference article Open Access OPEN
The 4SECURail approach to formalizing standard interfaces between signalling systems components
Belli D., Fantechi A., Gnesi S., Masullo L., Mazzanti F., Pistilli G., Quadrini L., Trentini D., Vaghi C.
In the context of the Shift2Rail open call S2R-OC-IP2-01-2019, one of the two work streams of the 4SECURail project (GA 881775) pursues the objective to corroborate how a clear, rigorous standard interface specification between signalling sub-systems can be designed by applying an approach based on semi-formal and formal methods. The objective is addressed by developing a demonstrator case study of the application of formal methods to the specification of standard interfaces, aimed at consolidating the most suitable techniques for rigorous standard interface specification, as well as at supporting a Cost-Benefit Analysis to back this strategy with sound economic arguments. This paper discusses the main results of the project.Source: Transport Research Arena (TRA) Conference, Lisbon, Portugal, 13-14/11/2022
Project(s): 4SECURAIL via OpenAIRE

See at: ISTI Repository Open Access | CNR ExploRA


2022 Conference article Open Access OPEN
ChAALenge: an ambient assisted living project to promote an active and health ageing
Barsocchi P., Belli D., Gabrielli E., La Rosa D., Miori V., Palumbo F., Russo D., Tolomei G.
The rapid growth of older population in the next years will lead to the rapid growth in the demand of health care, resulting in an increasing difficulty in managing hospitalizations and in a prohibitive grow of costs for medical care. In this context, chronic heart failure emerges as one of the most difficult problems to be treated, especially in advanced age, and a major cause of hospitalization and death. The Project ChAALenge aims at facing the problem by proposing a proactive approach based on pervasive monitoring and artificial intelligence. The goal is to promptly stepping, before the pathology onset, with effective suggestions ranging from the request of medical examination to the adjustment of lifestyle. The current paper presents the mid-term results of the ongoing project, introducing the sensors, the middleware and the candidate artificial intelligence techniques constituting the predictive system of the older adults' health status.Source: AIxIA 2022 - 21st International Conference of the Italian Association for Artificial Intelligence, pp. 42–58, Udine, Italy, 28/11/2022, 02/12/2022

See at: ceur-ws.org Open Access | ISTI Repository Open Access | CNR ExploRA


2022 Report Unknown
ChAALenge - D6.1: Analisi delle peculiarità di salute della popolazione anziana e definizione requisiti tecnici
Miori V., Belli D., Bacco M F., Baronti P., Barsocchi P., Crivello A., Furfari F., Girolami M., La Rosa D., Mavilia F., Palumbo F., Pillitteri L., Potortì F., Russo D.
In questo documento viene posta particolare attenzione alla malattia dello scompenso cardiaco che è una delle maggiori cause di mortalità e disabilità nella popolazione anziana oltre ad essere la prima causa di ricovero. Sono analizzate le soluzioni di monitoraggio domestico attualmente disponibili e i requisiti tecnici da soddisfare per poter raccogliere e analizzare i dati fisiologici nell'ambiente di vita e riconoscere situazioni di insorgenza o peggioramento di patologie nell'anziano.Source: ISTI Project Report, ChAALenge, D6.1, 2022

See at: CNR ExploRA


2022 Report Unknown
ChAALenge D5.2 - Documento di definizione degli algoritmi di Machine Learning e Deep Learning
Miori V., Belli D., Bacco F. M., Baronti P., Barsocchi P., Crivello A., Furfari F., Girolami M., La Rosa D., Mavilia F., Palumbo F., Pillitteri L., Potortì F., Russo D.
Il deliverable ha come obiettivo la definizione di un percorso intraprendibile per lo sviluppo di un modello predittivo, efficace ed efficiente, basato sul paradigma machine learning, sviluppato in funzione del dominio applicativo in esame e dei dati a disposizione. Una parte verrà dedicata all'introduzione degli aspetti principali legati alle strategie di individuazione di anomalie in serie temporali multi-variate tramite il suddetto modello predittivo.Source: ISTI Project Report, ChAALenge, D5.2, 2022

See at: CNR ExploRA


2022 Report Unknown
ChAALenge - D6.2: Progettazione architettura e definizione delle modalità di integrazione delle macrofunzionalità nel framework (intermedio)
Bacco F. M., Baronti P., Barsocchi P., Crivello A., Furfari F., Girolami M., La Rosa D., Mavilia F., Miori V., Palumbo F., Pillitteri L., Potortì F., Russo D., Belli D.
Questo documento riporta l'analisi relativa alla progettazione del framework di integrazione delle funzionalità, come previsto dal progetto ChAALenge. In particolare, vengono in questa sede analizzate le tecnologie per lo sviluppo del middleware di comunicazione e le modalità di interfacciamento con le soluzioni sensoristiche individuate.Source: ISTI Project Report, ChAALenge, D6.2, 2022

See at: CNR ExploRA


2021 Report Open Access OPEN
4SECURail - Technical Informative Note 15 - Progress Report: Formal development Demonstrator Prototype
Mazzanti F., Belli D.
This Technical Informative Note describes the progress of the activity of Work Package 2 / Task 2.3 in the months 12-17 of the project 4SECURail. The final results of Task 2.3 will be described in Deliverable 2.5, due at month 20 (end of July 2021). This Technical Informative Note is likely to already contain most of the interesting results that will appear in the final deliverable, together with other less important internal progress details that for readability issues will not appear in the final version. The overall final purpose of the whole experimentation is the observation of the impact, in our specific case, i.e. applying our specific tools and methodologies1 to our specific case study2, of the adoption of formal methods towards the improvement of the quality of the system specifications under construction.Source: Project report, 4SECURail, TIN-FM-15, pp.1–53, 2021
Project(s): 4SECURAIL via OpenAIRE

See at: ISTI Repository Open Access | CNR ExploRA


2021 Report Open Access OPEN
4SECURail - Revised requirements of the 4SECURail case study
Mazzanti F., Belli D.
The final version of the system requirements of the case study used in the 4SECURail demonstratorSource: ISTI Project report, 4SECURail, 2021
DOI: 10.5281/zenodo.5541217
Project(s): 4SECURAIL via OpenAIRE
Metrics:


See at: ISTI Repository Open Access | CNR ExploRA


2021 Software Unknown
Formal models of the SAI/CSL system of the 4SECURail case study
Mazzanti F., Belli D.
Formal models of 4SECURAIL case study in the notation accepted by UMC, ProB, CADP/LNTDOI: 10.5281/zenodo.5541307
Project(s): 4SECURAIL via OpenAIRE
Metrics:


See at: CNR ExploRA


2021 Software Unknown
The UMC2LNT and UMC2PROB model transformation tools
Mazzanti F., Belli D.
This documents contains the source code of two trasformation tools used in the 4SECURail project. The tools umc2lnt takes as argument the name of a file contining an UMC model and generates the corresponding CADP/LNT model.DOI: 10.5281/zenodo.5541350
Project(s): 4SECURAIL via OpenAIRE
Metrics:


See at: CNR ExploRA


2021 Journal article Open Access OPEN
How mobility and sociality reshape the context: a decade of experience in mobile crowdsensing
Girolami M., Belli D., Chessa S., Foschini L.
The possibility of understanding the dynamics of human mobility and sociality creates the opportunity to re-design the way data are collected by exploiting the crowd. We survey the last decade of experimentation and research in the field of mobile CrowdSensing, a paradigm centred on users' devices as the primary source for collecting data from urban areas. To this purpose, we report the methodologies aimed at building information about users' mobility and sociality in the form of ties among users and communities of users. We present two methodologies to identify communities: spatial and co-location-based. We also discuss some perspectives about the future of mobile CrowdSensing and its impact on four investigation areas: contact tracing, edge-based MCS architectures, digitalization in Industry 5.0 and community detection algorithms.Source: Sensors (Basel) 21 (2021). doi:10.3390/s21196397
DOI: 10.3390/s21196397
Metrics:


See at: ISTI Repository Open Access | www.mdpi.com Open Access | CNR ExploRA


2021 Report Open Access OPEN
4SECURail - Formal development demonstrator prototype, final release
Mazzanti F., Belli D.
This Deliverable describes the final results of Task 2.3 of 4SECURail project. The goal of Task 2.3 is to apply the formal development demonstrator process defined in Task 2.1 to the signalling case study defined in Task 2.2 and to describe the observed impact of the selected tools and methodologies for improving the quality of the system specifications under analysis.Source: ISTI Project report, 4SECURail, 2021
Project(s): 4SECURAIL via OpenAIRE

See at: ISTI Repository Open Access | CNR ExploRA


2020 Conference article Restricted
Impact of evolutionary community detection algorithms for edge selection strategies
Barsocchi P., Belli D., Chessa S., Foschini L., Girolami M.
The combination of the edge computing paradigm with Mobile CrowdSensing (MCS) is a promising approach. However, the selection of the proper edge nodes is a crucial aspect that greatly affects the performance of the extended architecture. This work studies the performance of an edge-based MCS architecture with ParticipAct, a real-word experimental dataset. We present a community-based edge selection strategy and we measure two key metrics, namely latency and the number of requests satisfied. We show how they vary by adopting three evolutionary community detection algorithms, TILES, Infomap and iLCD configured by changing several configuration settings. We also study the two metrics, by varying the number of edge nodes selected so that to show its benefit.Source: GLOBECOM 2020 - IEEE Global Communications Conference, Taipei, Taiwan, December 07-11, 2020
DOI: 10.1109/globecom42002.2020.9348085
Metrics:


See at: Archivio istituzionale della ricerca - Alma Mater Studiorum Università di Bologna Restricted | ieeexplore.ieee.org Restricted | xplorestaging.ieee.org Restricted | CNR ExploRA